\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $l$:IdLnk, ${\it tgs}$:Id List, ${\it ks}$:Knd List,\+
\\[0ex]$g$:($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$) \}$\rightarrow$(\=${\it tg}$:\{${\it tg}$:Id$\mid$ (${\it tg}$ $\in$ ${\it tgs}$) \}\+
\\[0ex]$\times$(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$(${\it da}$(rcv($l$,${\it tg}$))?Void List))) List).
\-\-\\[0ex]no\_repeats(Id;${\it tgs}$)
\\[0ex]$\Rightarrow$ ($\forall$${\it tg}$$\in$${\it tgs}$. rcv($l$,${\it tg}$) $\in$ dom(${\it da}$))
\\[0ex]$\Rightarrow$ (\=$\forall$${\it es}$:ES.\+
\\[0ex]($\forall$$k$$\in$${\it ks}$. sends $k$(v:${\it da}$($k$)?Void) on $l$:tagged($g$($k$),State(${\it ds}$),v):dt($l$;${\it da}$))
\\[0ex]\& ($\forall$${\it tg}$$\in$${\it tgs}$. only events in ${\it ks}$ send on $l$ with ${\it tg}$)
\\[0ex]$\Rightarrow$ es{-}decls(${\it es}$;source($l$);${\it ds}$;${\it da}$)
\\[0ex]$\Rightarrow$ \=with decls \=${\it ds}$ \+\+
\\[0ex]${\it da}$
\-\\[0ex]sends on $l$ from $e$ 
\\[0ex]include \=if \=deq{-}member(KindDeq;kind($e$);${\it ks}$)$\rightarrow$\+\+
\\[0ex]tagged{-}list{-}messages((state when $e$);val($e$);$g$(kind($e$)))
\-\\[0ex]else nil fi 
\-\\[0ex]and only these for tags in ${\it tgs}$)
\-\-
\end{tabbing}